1. Field of the Invention
The invention relates in general to designing of integrated circuits, and more particularly, to formal verification of low power integrated circuit designs.
2. Description of the Related Art
There is a growing need for enhanced power management capability in electronic devices, especially in battery-operated portable wireless devices such as cell phones, for example. Power management typically involves minimizing overall power consumption among different device functions. The intricacies of power management increase with the number and complexity of device functions.
Power management capabilities typically are built into a circuit design. Techniques to design-in power consumption management in an integrated circuit (IC) design include minimization of leakage power dissipation, design of efficient packaging and cooling systems and verification of functionality or power shut-off sequences early in the IC design process. For example, an integrated circuit can be partitioned into power domains, each of which contains circuit elements with similar power-related attributes, so that the power to each domain can be managed separately. Power management techniques that can be applied to power domains include the ability to power-up or power-down the circuit design blocks within a particular power domain as a group and the ability to a specify a particular voltage level for circuit design blocks within a power domain. Also, clock gating can be employed to save power by selectively turning off the clock signal controlling state elements that are not being used for a period of time.
In some designs, all the design blocks of a given power domain are switched on or off simultaneously. Modern hardware designs, which have very stringent power requirements, may have multiple power domains, so that parts of the design can be switched off when required to save power. A power domain may be switched on, later, when so required. Further, for some applications it is required that a power domain must come back up in same state as when it was powered down. Such capability typically is modeled using state retention elements in the design.
State retention elements, at the physical level, can be implemented in various different ways. For example, state may be retained by copying the state of state retention elements to other flip-flops or latches, which belong to a power domain that remains powered up when the power domain for which state is retained is powered off. Alternatively, state of state retention elements may be retained by copying the state of system to secondary memory. As yet another alternative, state may be copied to system memory by software.
The above approaches each involve creation of at least one additional state bit per state element whose state is to be retained. The additional state bit is used to save system state when the corresponding power domain is switched off. This might be the desirable solution for implementation flow and workable technique for verification of such circuits using simulation. However, creation of an additional state retention bit can severely impact Formal Verification of such designs.
Formal Verification is known to have complexity which is roughly exponential to the number of state bits in the circuit model. That is, every additional state retention bit approximately could double the complexity for formal verification.
Formal verification is a method of determining whether a design functions in a manner that satisfies its specification. Formal verification is distinguished from other functional verification methods, such as simulation, in that it typically considers all possible behaviors of the design for a given set of input constraints, rather than just considering one possible behavior at a time. This characteristic makes formal verification results much more comprehensive than typical simulation results. At the same time, this characteristic makes formal verification sensitive to the size of the state space of a design, which is a function of the number of state bits involved in the design.
Assertion-based verification captures the behavior required by a design's specification in the form of declarative statements called assertions. Functional verification tools (both simulation and formal verification) can then focus on determining whether a given assertion “holds” for a given design, i.e., whether the design satisfies the assertion by always behaving in a manner that is consistent with the assertion.
Assertion-based formal verification involves proving that assertions hold for all possible states of the design. The possible states are those that are reachable from the design's initial state, given a particular set of input constraints. Assertions can describe required behavior of a design independent of any power control activity, or they can describe behavior specific to the operation of power control circuitry.
In both cases, the ability to formally verify that the design is behaving in a manner that is consistent with its assertions depends upon having an accurate and efficient model representing the addition of power control circuitry to the design. Thus, there has been a need for an accurate and efficient model, that accurately models the effects of power shutoff when applied to state elements, and that models these effects without adding additional state bits to the verification model that could exponentially increase the design's state space. The present invention meets this need.